\begin{tabbing}
$\forall$${\it es}$:ES, $L$:(E List).
\\[0ex]$\exists$\=${\it L'}$:E List\+
\\[0ex]($L$ $\subseteq$ ${\it L'}$
\\[0ex]\& ${\it L'}$ $\subseteq$ $L$
\\[0ex]\& ($\forall$$a$, $b$:E. ($a$ $\in$ ${\it L'}$) $\Rightarrow$ ($b$ $\in$ ${\it L'}$) $\Rightarrow$ ($a$ $<$ $b$) $\Rightarrow$ $a$ before $b$ $\in$ ${\it L'}$)
\\[0ex]\& no\_repeats(E;${\it L'}$))
\-
\end{tabbing}